$\forall$${\it ds}$:(Id$\rightarrow$Type), ${\it da}$:(Id$\rightarrow$Knd$\rightarrow$Type), $A$, $B$:Type, $X$:Interface(${\it ds}$;${\it da}$;$A$), $Y$:Interface(${\it ds}$;${\it da}$;$B$).
\\[0ex]interface{-}union($X$;$Y$) $\in$ Interface(${\it ds}$;${\it da}$;$A$ + $B$)